A, B:Realizer. R-icompat(A;B)  Prop 

latex

Definitions	R-interface-compat(A;B), x:AB(x), P & Q, True, Type, R-loc(R), Id, s = t, b, A, b, , a = b, x:AB(x), P  Q, Unit, left+right, Rnone?(x1), #$n, n-m, , Rplus-right(x1), {x:A| B(x) }, Rplus-left(x1), {T}, Rplus?(x1), False, a<b, Void, , ij, -n, R-size(R), n+m, R-icompat(A;B), Prop, t  T, AB, P  Q, Realizer, x:A. B(x),
Lemmas	ge wf, nat properties, nat wf, le wf, es realizer wf, Rplus? wf, R-size-decreases, Rplus-left wf, R-size wf, Rplus-right wf, nat plus wf, Rnone? wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, eq id wf, bool wf, bnot wf, not wf, assert wf, Id wf, R-loc wf, true wf, R-interface-compat wf